This paper was randomly selected as your next reading.

Automated Verification of Fundamental Algebraic Laws

Algebraic laws of functions in mathematics such as commutativity, associativity, and idempotence are often used as the basis to derive more sophisticated properties of complex mathematical structures and are heavily used in abstract computational thinking. Algebraic laws of functions in coding , however, are rarely considered. Yet, they are essential. For example, commutativity and associativity are crucial to ensure correctness of a variety of software systems in numerous domains, such as compiler optimization, big data processing, data flow processing, machine learning or distributed algorithms and data structures. Still, most programming languages lack builtin mechanisms to enforce and verify that operations adhere to such properties. In this paper, we propose a verifier specialized on a set of fundamental algebraic laws that ensures that such laws hold in application code. The verifier can conjecture auxiliary properties and can reason about both equalities and inequalities of expressions, which is crucial to prove a given property when other competitors do not succeed. We implement these ideas in the Propel verifier. Our evaluation against five stateoftheart verifiers on a

Zakhour, George, et al. “Automated Verification of Fundamental Algebraic Laws. Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, June 2024, pp. 76689. Crossref, https://doi.org/10.1145/3656408.

Merge this PR to apply selection.